i, a, x:Id, A, T:Type, P:(ATProp).
@i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  Dsys
& (D:Dsys.
& (@i: ma-single-pre1(x;A;a;T;x,v.P(x,v))  D
& ( D 
& ( realizes es.
& ( vartype(i;x)  A & (e:E. loc(e) = i  Id  kind(e) = locl(a)  Knd  valtype(e)  T)
& ( & (e:E.
& ( & (loc(e) = i  Id
& ( & ( (kind(e) = locl(a)  Knd  P(x when e,val(e)))
& ( & ( & (e':E.
& ( & ( & ((e <loc e')  e = e'  E
& ( & ( & (& kind(e') = locl(a)  Knd  (v:T. P((x after e'),v))))) 

latex

Definitions

t  T, P  Q, x:A. B(x), A & B, ES(the_w), E, s = t, (e <loc e'), left+right, Void, x:AB(x), Knd, x:AB(x), x:A. B(x), False, P  Q, A, 1of(t), IdDeq, Id, x:A. B(x), Top, Atom$n, Type, Dsys, D1  D2, World, P & Q, FairFifo, PossibleWorld(D;w), loc(e), Prop, locl(a), kind(e), valtype(e), vartype(i;x), s.x, (x after e), x when e, e@i. P(e), ee'.P(e'), @i Precondition for a(v)P State(ds) (v:T), D realizes es. P(es), x. t(x), State(ds), f(x)?z, ma-single-pre1(x;A;a;T;y,v.P(y;v)), f(a), x(s1,s2), x.A(x), x : v

Lemmas

s-pre-rule, fpf-cap-single1, top wf, subtype rel self, ma-state wf, fpf-single wf, dsys wf, d-sub wf, world wf, fair-fifo wf, possible-world wf, Knd wf, es-kind wf, locl wf, es-loc wf, es-E wf, w-es wf, fpf-cap-single, eqof eq btrue, Id wf, id-deq wf